; benchmark generated from python API
(set-info :status unknown)
(declare-fun basic_right_bottom_feasible () Bool)
(declare-fun basic_right_bottom_kid_4_feasible () Bool)
(declare-fun basic_right_bottom_kid_3_feasible () Bool)
(declare-fun basic_right_bottom_kid_2_feasible () Bool)
(declare-fun basic_right_bottom_kid_1_feasible () Bool)
(declare-fun basic_right_bottom_kid_0_feasible () Bool)
(declare-fun basic_right_bottom_kid_4_width () Real)
(declare-fun basic_right_bottom_kid_0_width () Real)
(declare-fun basic_right_bottom_kid_3_width () Real)
(declare-fun basic_right_bottom_kid_2_width () Real)
(declare-fun basic_right_bottom_kid_1_width () Real)
(declare-fun basic_right_bottom_kid_3_x () Real)
(declare-fun basic_right_bottom_kid_4_x () Real)
(declare-fun basic_right_bottom_kid_2_x () Real)
(declare-fun basic_right_bottom_kid_1_x () Real)
(declare-fun basic_right_bottom_kid_0_x () Real)
(declare-fun basic_right_bottom_hight () Real)
(declare-fun basic_right_bottom_kid_4_hight () Real)
(declare-fun basic_right_bottom_kid_4_y () Real)
(declare-fun basic_right_bottom_kid_3_hight () Real)
(declare-fun basic_right_bottom_kid_3_y () Real)
(declare-fun basic_right_bottom_kid_2_hight () Real)
(declare-fun basic_right_bottom_kid_2_y () Real)
(declare-fun basic_right_bottom_kid_1_hight () Real)
(declare-fun basic_right_bottom_kid_1_y () Real)
(declare-fun basic_right_bottom_kid_0_hight () Real)
(declare-fun basic_right_bottom_kid_0_y () Real)
(declare-fun basic_right_bottom_width () Real)
(assert
 (let (($x2204 (= (- basic_right_bottom_kid_0_width basic_right_bottom_kid_4_width) 0.0)))
 (let (($x2202 (= (- basic_right_bottom_kid_0_width basic_right_bottom_kid_3_width) 0.0)))
 (let (($x2200 (= (+ (- basic_right_bottom_kid_2_width) basic_right_bottom_kid_0_width) 0.0)))
 (let (($x2198 (= (- basic_right_bottom_kid_0_width basic_right_bottom_kid_1_width) 0.0)))
 (let ((?x2167 (- (- basic_right_bottom_kid_4_x basic_right_bottom_kid_3_x) basic_right_bottom_kid_3_width)))
 (let (($x2196 (= ?x2167 10.0)))
 (let ((?x2164 (- (+ (- basic_right_bottom_kid_2_width) basic_right_bottom_kid_3_x) basic_right_bottom_kid_2_x)))
 (let (($x2195 (= ?x2164 10.0)))
 (let ((?x2161 (+ (- (- basic_right_bottom_kid_1_width) basic_right_bottom_kid_1_x) basic_right_bottom_kid_2_x)))
 (let (($x2194 (= ?x2161 10.0)))
 (let ((?x2157 (+ (- (- basic_right_bottom_kid_0_x) basic_right_bottom_kid_0_width) basic_right_bottom_kid_1_x)))
 (let (($x2193 (= ?x2157 10.0)))
 (let ((?x2191 (- (+ basic_right_bottom_kid_4_y basic_right_bottom_kid_4_hight) basic_right_bottom_hight)))
 (let (($x2192 (= ?x2191 0.0)))
 (let ((?x2188 (- (+ basic_right_bottom_kid_3_y basic_right_bottom_kid_3_hight) basic_right_bottom_hight)))
 (let (($x2189 (= ?x2188 0.0)))
 (let ((?x2185 (- (+ basic_right_bottom_kid_2_y basic_right_bottom_kid_2_hight) basic_right_bottom_hight)))
 (let (($x2186 (= ?x2185 0.0)))
 (let ((?x2182 (+ (- basic_right_bottom_kid_1_y basic_right_bottom_hight) basic_right_bottom_kid_1_hight)))
 (let (($x2183 (= ?x2182 0.0)))
 (let ((?x2179 (+ (- basic_right_bottom_kid_0_y basic_right_bottom_hight) basic_right_bottom_kid_0_hight)))
 (let (($x2180 (= ?x2179 0.0)))
 (let (($x2177 (= basic_right_bottom_kid_4_y 0.0)))
 (let (($x2176 (= basic_right_bottom_kid_3_y 0.0)))
 (let (($x2175 (= basic_right_bottom_kid_2_y 0.0)))
 (let (($x2174 (= basic_right_bottom_kid_1_y 0.0)))
 (let (($x2173 (= basic_right_bottom_kid_0_y 0.0)))
 (let ((?x2171 (+ (+ (- basic_right_bottom_width) basic_right_bottom_kid_4_x) basic_right_bottom_kid_4_width)))
 (let (($x2172 (= ?x2171 0.0)))
 (let (($x2169 (= basic_right_bottom_kid_0_x 0.0)))
 (let (($x2168 (>= ?x2167 0.0)))
 (let (($x2165 (>= ?x2164 0.0)))
 (let (($x2162 (>= ?x2161 0.0)))
 (let (($x2158 (>= ?x2157 0.0)))
 (let ((?x2154 (+ (- (- basic_right_bottom_kid_4_y) basic_right_bottom_kid_4_hight) basic_right_bottom_hight)))
 (let (($x2155 (>= ?x2154 0.0)))
 (let (($x2116 (>= basic_right_bottom_kid_4_y 0.0)))
 (let ((?x2150 (- (- basic_right_bottom_width basic_right_bottom_kid_4_x) basic_right_bottom_kid_4_width)))
 (let (($x2151 (>= ?x2150 0.0)))
 (let (($x2115 (>= basic_right_bottom_kid_4_x 0.0)))
 (let ((?x2147 (+ (- (- basic_right_bottom_kid_3_y) basic_right_bottom_kid_3_hight) basic_right_bottom_hight)))
 (let (($x2148 (>= ?x2147 0.0)))
 (let (($x2112 (>= basic_right_bottom_kid_3_y 0.0)))
 (let ((?x2143 (- (- basic_right_bottom_width basic_right_bottom_kid_3_x) basic_right_bottom_kid_3_width)))
 (let (($x2144 (>= ?x2143 0.0)))
 (let (($x2111 (>= basic_right_bottom_kid_3_x 0.0)))
 (let ((?x2140 (+ (- (- basic_right_bottom_kid_2_y) basic_right_bottom_kid_2_hight) basic_right_bottom_hight)))
 (let (($x2141 (>= ?x2140 0.0)))
 (let (($x2108 (>= basic_right_bottom_kid_2_y 0.0)))
 (let ((?x2136 (- (+ (- basic_right_bottom_kid_2_width) basic_right_bottom_width) basic_right_bottom_kid_2_x)))
 (let (($x2137 (>= ?x2136 0.0)))
 (let (($x2107 (>= basic_right_bottom_kid_2_x 0.0)))
 (let ((?x2132 (- (+ (- basic_right_bottom_kid_1_y) basic_right_bottom_hight) basic_right_bottom_kid_1_hight)))
 (let (($x2133 (>= ?x2132 0.0)))
 (let (($x2104 (>= basic_right_bottom_kid_1_y 0.0)))
 (let ((?x2128 (- (- basic_right_bottom_width basic_right_bottom_kid_1_width) basic_right_bottom_kid_1_x)))
 (let (($x2129 (>= ?x2128 0.0)))
 (let (($x2103 (>= basic_right_bottom_kid_1_x 0.0)))
 (let ((?x2125 (- (+ (- basic_right_bottom_kid_0_y) basic_right_bottom_hight) basic_right_bottom_kid_0_hight)))
 (let (($x2126 (>= ?x2125 0.0)))
 (let (($x2100 (>= basic_right_bottom_kid_0_y 0.0)))
 (let ((?x2121 (- (+ (- basic_right_bottom_kid_0_x) basic_right_bottom_width) basic_right_bottom_kid_0_width)))
 (let (($x2122 (>= ?x2121 0.0)))
 (let (($x2099 (>= basic_right_bottom_kid_0_x 0.0)))
 (let (($x2118 (>= basic_right_bottom_kid_4_hight 0.0)))
 (let (($x2117 (>= basic_right_bottom_kid_4_width 0.0)))
 (let (($x2114 (>= basic_right_bottom_kid_3_hight 0.0)))
 (let (($x2113 (>= basic_right_bottom_kid_3_width 0.0)))
 (let (($x2110 (>= basic_right_bottom_kid_2_hight 0.0)))
 (let (($x2109 (>= basic_right_bottom_kid_2_width 0.0)))
 (let (($x2106 (>= basic_right_bottom_kid_1_hight 0.0)))
 (let (($x2105 (>= basic_right_bottom_kid_1_width 0.0)))
 (let (($x2102 (>= basic_right_bottom_kid_0_hight 0.0)))
 (let (($x2101 (>= basic_right_bottom_kid_0_width 0.0)))
 (and $x2099 $x2100 $x2101 $x2102 $x2103 $x2104 $x2105 $x2106 $x2107 $x2108 $x2109 $x2110 $x2111 $x2112 $x2113 $x2114 $x2115 $x2116 $x2117 $x2118 $x2099 $x2122 $x2100 $x2126 $x2103 $x2129 $x2104 $x2133 $x2107 $x2137 $x2108 $x2141 $x2111 $x2144 $x2112 $x2148 $x2115 $x2151 $x2116 $x2155 $x2158 $x2162 $x2165 $x2168 $x2169 $x2172 $x2173 $x2174 $x2175 $x2176 $x2177 $x2180 $x2183 $x2186 $x2189 $x2192 $x2193 $x2194 $x2195 $x2196 $x2198 $x2200 $x2202 $x2204 basic_right_bottom_kid_0_feasible basic_right_bottom_kid_1_feasible basic_right_bottom_kid_2_feasible basic_right_bottom_kid_3_feasible basic_right_bottom_kid_4_feasible basic_right_bottom_feasible))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

